The success of Conflict Driven Clause Learning (CDCL) forBoolean satisfiability has inspired adoption in other domains. We presenta novel lifting of CDCL to program analysis called Abstract ConflictDriven Learning for Programs (ACDLP). ACDLP alternates betweenmodel search, which performs over-approximate deduction with constraintpropagation, and conflict analysis, which performs under-approximateabduction with heuristic choice. We instantiate the model search andconflict analysis algorithms to an abstract domain of template polyhedra,strictly generalizing CDCL from the Boolean lattice to a richer latticestructure. Our template polyhedra can express intervals, octagons andrestricted polyhedral constraints over program variables. We have implementedACDLP for automatic bounded safety verification of C programs.We evaluate the performance of our analyser by comparing with CBMC,which uses Boolean CDCL, and Astr´ee, a commercial abstract interpretationtool. We observe two orders of magnitude reduction in the numberof decisions, propagations, and conflicts as well as a 1.5x speedup inruntime compared to CBMC. Compared to Astr´ee, ACDLP solves twiceas many benchmarks and has much higher precision. This is the firstinstantiation of CDCL with a template polyhedra abstract domain.
展开▼
